0 Prolog
↳1 PrologToPiTRSProof (⇒, 0 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 11 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 MRRProof (⇔, 47 ms)
↳27 QDP
↳28 PisEmptyProof (⇔, 0 ms)
↳29 YES
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
QUERY_IN_G(XS) → U6_G(XS, shuffle_in_ga(cons(X, XS), YS))
QUERY_IN_G(XS) → SHUFFLE_IN_GA(cons(X, XS), YS)
SHUFFLE_IN_GA(cons(X, XS), cons(X, YS)) → U4_GA(X, XS, YS, reverse_in_ga(XS, ZS))
SHUFFLE_IN_GA(cons(X, XS), cons(X, YS)) → REVERSE_IN_GA(XS, ZS)
REVERSE_IN_GA(cons(X, XS), YS) → U2_GA(X, XS, YS, reverse_in_ga(XS, ZS))
REVERSE_IN_GA(cons(X, XS), YS) → REVERSE_IN_GA(XS, ZS)
U2_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_GA(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
U2_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → APPEND_IN_GGA(ZS, cons(X, nil), YS)
APPEND_IN_GGA(cons(X, XS), YS, cons(X, ZS)) → U1_GGA(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
APPEND_IN_GGA(cons(X, XS), YS, cons(X, ZS)) → APPEND_IN_GGA(XS, YS, ZS)
U4_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_GA(X, XS, YS, shuffle_in_ga(ZS, YS))
U4_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → SHUFFLE_IN_GA(ZS, YS)
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
QUERY_IN_G(XS) → U6_G(XS, shuffle_in_ga(cons(X, XS), YS))
QUERY_IN_G(XS) → SHUFFLE_IN_GA(cons(X, XS), YS)
SHUFFLE_IN_GA(cons(X, XS), cons(X, YS)) → U4_GA(X, XS, YS, reverse_in_ga(XS, ZS))
SHUFFLE_IN_GA(cons(X, XS), cons(X, YS)) → REVERSE_IN_GA(XS, ZS)
REVERSE_IN_GA(cons(X, XS), YS) → U2_GA(X, XS, YS, reverse_in_ga(XS, ZS))
REVERSE_IN_GA(cons(X, XS), YS) → REVERSE_IN_GA(XS, ZS)
U2_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_GA(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
U2_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → APPEND_IN_GGA(ZS, cons(X, nil), YS)
APPEND_IN_GGA(cons(X, XS), YS, cons(X, ZS)) → U1_GGA(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
APPEND_IN_GGA(cons(X, XS), YS, cons(X, ZS)) → APPEND_IN_GGA(XS, YS, ZS)
U4_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_GA(X, XS, YS, shuffle_in_ga(ZS, YS))
U4_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → SHUFFLE_IN_GA(ZS, YS)
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
APPEND_IN_GGA(cons(X, XS), YS, cons(X, ZS)) → APPEND_IN_GGA(XS, YS, ZS)
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
APPEND_IN_GGA(cons(X, XS), YS, cons(X, ZS)) → APPEND_IN_GGA(XS, YS, ZS)
APPEND_IN_GGA(cons(XS), YS) → APPEND_IN_GGA(XS, YS)
From the DPs we obtained the following set of size-change graphs:
REVERSE_IN_GA(cons(X, XS), YS) → REVERSE_IN_GA(XS, ZS)
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
REVERSE_IN_GA(cons(X, XS), YS) → REVERSE_IN_GA(XS, ZS)
REVERSE_IN_GA(cons(XS)) → REVERSE_IN_GA(XS)
From the DPs we obtained the following set of size-change graphs:
U4_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → SHUFFLE_IN_GA(ZS, YS)
SHUFFLE_IN_GA(cons(X, XS), cons(X, YS)) → U4_GA(X, XS, YS, reverse_in_ga(XS, ZS))
query_in_g(XS) → U6_g(XS, shuffle_in_ga(cons(X, XS), YS))
shuffle_in_ga(nil, nil) → shuffle_out_ga(nil, nil)
shuffle_in_ga(cons(X, XS), cons(X, YS)) → U4_ga(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
U4_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U5_ga(X, XS, YS, shuffle_in_ga(ZS, YS))
U5_ga(X, XS, YS, shuffle_out_ga(ZS, YS)) → shuffle_out_ga(cons(X, XS), cons(X, YS))
U6_g(XS, shuffle_out_ga(cons(X, XS), YS)) → query_out_g(XS)
U4_GA(X, XS, YS, reverse_out_ga(XS, ZS)) → SHUFFLE_IN_GA(ZS, YS)
SHUFFLE_IN_GA(cons(X, XS), cons(X, YS)) → U4_GA(X, XS, YS, reverse_in_ga(XS, ZS))
reverse_in_ga(nil, nil) → reverse_out_ga(nil, nil)
reverse_in_ga(cons(X, nil), cons(X, nil)) → reverse_out_ga(cons(X, nil), cons(X, nil))
reverse_in_ga(cons(X, XS), YS) → U2_ga(X, XS, YS, reverse_in_ga(XS, ZS))
U2_ga(X, XS, YS, reverse_out_ga(XS, ZS)) → U3_ga(X, XS, YS, append_in_gga(ZS, cons(X, nil), YS))
U3_ga(X, XS, YS, append_out_gga(ZS, cons(X, nil), YS)) → reverse_out_ga(cons(X, XS), YS)
append_in_gga(nil, XS, XS) → append_out_gga(nil, XS, XS)
append_in_gga(cons(X, XS), YS, cons(X, ZS)) → U1_gga(X, XS, YS, ZS, append_in_gga(XS, YS, ZS))
U1_gga(X, XS, YS, ZS, append_out_gga(XS, YS, ZS)) → append_out_gga(cons(X, XS), YS, cons(X, ZS))
U4_GA(reverse_out_ga(ZS)) → SHUFFLE_IN_GA(ZS)
SHUFFLE_IN_GA(cons(XS)) → U4_GA(reverse_in_ga(XS))
reverse_in_ga(nil) → reverse_out_ga(nil)
reverse_in_ga(cons(nil)) → reverse_out_ga(cons(nil))
reverse_in_ga(cons(XS)) → U2_ga(reverse_in_ga(XS))
U2_ga(reverse_out_ga(ZS)) → U3_ga(append_in_gga(ZS, cons(nil)))
U3_ga(append_out_gga(YS)) → reverse_out_ga(YS)
append_in_gga(nil, XS) → append_out_gga(XS)
append_in_gga(cons(XS), YS) → U1_gga(append_in_gga(XS, YS))
U1_gga(append_out_gga(ZS)) → append_out_gga(cons(ZS))
reverse_in_ga(x0)
U2_ga(x0)
U3_ga(x0)
append_in_gga(x0, x1)
U1_gga(x0)
U4_GA(reverse_out_ga(ZS)) → SHUFFLE_IN_GA(ZS)
SHUFFLE_IN_GA(cons(XS)) → U4_GA(reverse_in_ga(XS))
reverse_in_ga(nil) → reverse_out_ga(nil)
reverse_in_ga(cons(nil)) → reverse_out_ga(cons(nil))
reverse_in_ga(cons(XS)) → U2_ga(reverse_in_ga(XS))
U2_ga(reverse_out_ga(ZS)) → U3_ga(append_in_gga(ZS, cons(nil)))
U3_ga(append_out_gga(YS)) → reverse_out_ga(YS)
append_in_gga(nil, XS) → append_out_gga(XS)
append_in_gga(cons(XS), YS) → U1_gga(append_in_gga(XS, YS))
U1_gga(append_out_gga(ZS)) → append_out_gga(cons(ZS))
SHUFFLEINGA1 > appendingga2 > U1gga1 > nil > U4GA1 > appendoutgga1 > reverseinga1 > U2ga1 > U3ga1 > cons1 > reverseoutga1
nil=1
reverse_in_ga_1=4
reverse_out_ga_1=4
cons_1=3
U2_ga_1=3
U3_ga_1=2
append_out_gga_1=2
U1_gga_1=3
U4_GA_1=1
SHUFFLE_IN_GA_1=2
append_in_gga_2=1
reverse_in_ga(x0)
U2_ga(x0)
U3_ga(x0)
append_in_gga(x0, x1)
U1_gga(x0)